Sau đây là ứng dụng lôgic BAN vào phân tích giao thức giao thức Wide Mouth Frog, một giao thức đơn giản cho phép 2 thực thể, A và B, thiết lập một kênh truyền thông an toàn với sự tham gia của một máy chủ xác thực và các đồng hồ được đồng bộ hóa.

A và B đều có chung khóa (đối xứng) với máy chủ S: Kas và Kbs. Vì thế, ta có thể giả định:

A believes key(Kas, A<->S)S believes key(Kas, A<->S)B believes key(Kbs, B<->S)S believes key(Kbs, B<->S)

A muốn thiết lập một giao dịch với B. A tạo ra một khóa phiên Kab dùng để mật mã hóa các gói tin trao đổi với B. A tin rằng khóa này là an toàn vì khóa do chính mình tạo nên:

A believes key(Kab, A<->B)

B sẽ chấp nhận khóa nếu như anh ta tin rằng khóa thực sự là do A gửi đến:

B believes (A has jurisdiction over key(K, A<->B))

Ngoài ra, B cũng tin S sẽ chuyển những thông tin từ A một cách chính xác;

B believes (S has jurisdiction over (A believes key(K, A<->B)))

Do đó, nếu B cho rằng S tin rằng A muốn dùng một khóa nhất định để trao đổi thông tin với B thì B sẽ tin S và khóa được gửi đến.

Mục tiêu của giao thức là:

B believes key(Kab, A<->B)

Quá trình thực hiện giao thức như sau:

Đầu tiên, A xác định thời gian hiện tại t, và gửi gói tin:

1. A->S: {t, key(Kab, A<->B)}Kas

Gói tin bao gồm thời gian hiện tại cùng với khóa phiên do A chọn, tất cả được mật mã hóa với khóa chung giữa A và S - Kas.

Do S believes that key(Kas, A<->S) và S sees {t, key(Kab, A<->B)}Kas nên S kết luận rằng A thực tế đã gửi {t, key(Kab, A<->B)}. Có nghĩa là S tin rằng gói tin này không phải do một kẻ tấn công nào đó tạo ra.

Vì tất cả đồng hồ được đồng bộ hóa, ta có thể giả định:

S believes fresh(t)

Do S believes fresh(t) và S believes A said {t, key(Kab, A<->B)}, nênS tin rằng A thực sự tin (believes) vào key(Kab, A<->B). (Cụ thể hơn, S tin rằng gói tin đã không bị một kẻ tấn công nào đó gửi lại.)

Sau đó S chuyển khóa phiên tới B:

2. S->B: {t, A, A believes key(Kab, A<->B)}Kbs

Do gói tin 2 được mật mã hóa với Kbs và Bbelieves key(Kbs, B<->S) nên B tin rằng Ssaid {t, A, A believes key(Kab, A<->B)}. Do các đồng hồ được đồng bộ hóa nên B believes fresh(t) và fresh(A believes key(Kab, A<->B)). Do B tin rằng gói tin của S gửi đến là mới nên B cũng tin rằng S believes (A believes key(Kab, A<->B)). Vì B tin vào S nên B believes (A believes key(Kab, A<->B)). Vì thế, B believes key(Kab, A<->B). Lúc này B có thể liên lạc trực tiếp với A sử dụng khóa phiên Kab.

Bây giờ ta giả sử các đồng hồ không được đồng bộ. Trong trường hợp này S nhận gói tin thứ nhất từ A: {t, key(Kab, A<->B)} nhưng không thể kết luận gói tin này có mới hay không. S chỉ biết được rằng A đã từng tạo ra gói tin trên trong quá khứ (vì gói tin được mật mã hóa bằng khóa bí mật của A) nhưng không thể xác định được hiện tại A có còn muốn sử dụng khóa phiên Kab nữa hay không. Vì vậy, một kẻ tấn công có thể lợi dụng điểm yếu này: kẻ tấn công có thể lấy được một khóa phiên cũ (việc này tốn nhiều thời gian) và gửi lại gói tin {t, key(Kab, A<->B)}. Khi đó, S có thể không phát hiện được đây là gói tin gửi lại (do đồng hồ không đồng bộ) và chuyển tới B một khóa phiên cũ đã bị lộ.

Bài nghiên cứu gốc Logic of Authentication (xem liên kết ở phần sau) có bao gồm ví dụ trên cùng một số những dẫn chứng khác như phân tích giao thức Kerberos và 2 phiên bản của giao thức bắt tay Andrew RPC (trong đó có 1 giao thức có lỗi).